(***************************************************************************
 * Cast-Free Featherweight Java
 *
 * Bruno De Fraine, with help from Erik Ernst and Mario Sudholt, Summer 2008
 ***************************************************************************)

Require Import AdditionalTactics.
Require Import Metatheory.
Require Import FJ_Definitions.
Require Import FJ_Facts.

Lemma eval_bound_weak:
  forall F E G B C,
    ok (F ++ E ++ G) ->
    eval_bound (F ++ G) B C ->
    eval_bound (F ++ E ++ G) B C.
Proof.
  intros.
  case B, C;
    inversion H0;
    subst;
    eauto.
  apply (binds_weaken G E F) in H4.
  eauto.
  assumption.
  apply (binds_weaken G E F) in H3.
  eauto.
  assumption.
Qed.

Hint Resolve eval_bound_weak.

Lemma ok_type_weaken:
  forall F E G t A,
    ok (F ++ E ++ G) ->
    ok_type (F ++ G) t A ->
    ok_type (F ++ E ++ G) t A.
Proof.
  intros.
  induction H0.
  eauto.
  eauto.
  eauto.
  eauto.
  apply wf_var with (C:=C).
  apply (binds_weaken G E F) in H0.
  assumption.
  assumption.
  assumption.
  apply (wf_absfam (F++E++G) X C D).
  assumption.
  apply (binds_weaken G E F) in H1.
  assumption.
  assumption.
  assumption.
  eauto.
Qed.

Hint Resolve ok_type_weaken.

Lemma sub_weak:
  forall F E G t t',
    ok (F ++ E ++ G) ->
    sub (F ++ G) t t' ->
    sub (F ++ E ++ G) t t'.
Proof.
  intros.
  induction H0; subst.
  eauto.
  apply s_var.
  apply (binds_weaken G E F) in H0.
  assumption.
  assumption.
  apply s_object.
  eauto.
  eauto.
Qed.

Hint Resolve sub_weak.

Lemma subs_weak:
  forall l l' F E G,
    ok (F ++ E ++ G) ->
    subs (F ++ G) l l' ->
    subs (F ++ E ++ G) l l'.
Proof.
  intros l.
  induction l;
    intros.
    inversion H0; subst.
    eauto.
  destruct l'.
    inversion H0.
  inversion H0; subst.
  apply subs_cons.
    apply sub_weak; eauto.
  apply (IHl); eauto.
Qed.

Hint Resolve subs_weak.

Lemma weakening':
    (forall EE tE e t A, 
       typing EE tE e t A ->
       forall E F G, 
         EE = F++G -> 
         ok (F++E++G) -> 
         typing (F++E++G) tE e t A) /\
    (forall EE tE e t A, 
       wide_typing EE tE e t A ->
       forall E F G, 
         EE = F++G -> 
         ok (F++E++G) -> 
         wide_typing (F++E++G) tE e t A) /\
    (forall EE tE es env A, 
       wide_typings EE tE es env A ->
       forall E F G, 
         EE = F++G -> 
         ok (F++E++G) -> 
         wide_typings (F++E++G) tE es env A).
Proof.
  apply typings_mutind;
  intros;
  subst;
  eauto using binds_weaken;
  eapply t_invk;
  eauto.
Qed.

Hint Resolve weakening'.

Lemma weakening: 
  forall E tE F G e t A,
    ok (F++E++G) ->
    typing (F++G) tE e t A ->
    typing (F++E++G) tE e t A.
Proof.
  intros.
  destruct weakening' as (Hweak, _).
  eapply Hweak; 
    trivial; 
    assumption.
Qed.

Hint Resolve weakening.

(** * Requirements for preservation *)

(** ** Preservation over [exps_context] and [exp_context] *)
Fact preservation_over_esc: 
  forall EE E tE ts e e' A,
    exps_context EE ->
    (forall t', typing E tE e t' A -> 
                wide_typing E tE e' t' A) ->
    wide_typings E tE (EE e) ts A ->
    wide_typings E tE (EE e') ts A.
Proof.
  intros. 
  generalize dependent ts.
  induction H; 
    intros; 
    inversion H1; 
    subst.
  
  destruct H9.
  apply wts_cons.
  assumption.
  assumption.

  assert (H5 := H0 t H2).
  destruct H5.
  apply (s_trans E t t'0 t') in H4.
  apply wt_sub with (t':=t') in H7.
  assumption.
  assumption.
  assumption.
  assumption.

  apply wts_cons.
  assumption.
  apply IHexps_context.
  assumption.
  assumption.
Qed.

Module Properties (H: Hyps).
  (** Import previous conclusions for either of the hypotheses *)
  Module Import Facts1 := OkTableAndNoObjFacts H.

  Lemma sub_t_x:
    forall E T X x,
      sub E T X ->
      X = t_X x ->
      T = X.
  Proof.
    intros E T X x H.
    revert x.
    induction H; 
      intros;
      subst.
            reflexivity.
          inversion H0.
        inversion H.
      assert (IH2 := IHsub2 x eq_refl).
      assert (IH1 := IHsub1 x IH2).
      subst.
      reflexivity.
    inversion H0.
  Qed.

  Hint Resolve sub_t_x.

  Fact preservation_over_ec: 
    forall EE E tE e e' t A,
      exp_context EE ->
      (forall t0,
         typing E tE e t0 A -> 
         wide_typing E tE e' t0 A) ->
      typing E tE (EE e) t A ->
      wide_typing E tE (EE e') t A.
  Proof.
    intros.
    assert (typeis_qcname A). 
      inversion H1; subst; eauto.

    destruct H;
      inversion H1; 
      subst;
      eauto using preservation_over_esc.
    assert (He' := H0 T0 H13).
    inversion He'; subst.
    destruct B.
            inversion H6; subst.
            inversion H10; subst.
            eauto.
          inversion H10; subst.
          assert (HX := sub_t_x E t0 (t_X t1) t1 H8 eq_refl).
          subst.
          eauto.
        inversion H6; subst.
        inversion H10; subst.
          assert (H8' := sub_t_nested _ _ _ H8 (tin3 s0)).
          subst.
          eauto.
        assert (H8' := sub_t_nested _ _ _ H8 (tin1 s s0)).
        subst.
        eauto.
      inversion H10; subst.
        assert (H8' := sub_t_nested _ _ _ H8 (tin3 s)).
        subst.
        eauto.
      assert (H8' := sub_t_nested _ _ _ H8 (tin2 t1 s)).
      subst.
      eauto.
    inversion H6; subst.
    inversion H10; subst.
    assert (H8' := sub_t_nested _ _ _ H8 (tin3 s)).
    subst.
    eauto.
  Qed.
  
  Lemma binds_implies_get:
    forall E x (v:exp),
      binds x v E -> get x E = Some v.
  Proof.
    intros.
    eauto.
  Qed.

  Hint Resolve binds_implies_get.

  Lemma wts_implies_ok_E:
    forall E tE es ts A,
      wide_typings E tE es ts A ->
      ok E.
  Proof.
    intros.
    induction H; eauto.
  Qed.

  Hint Resolve wts_implies_ok_E.

  (** ** Term substitutivity lemma *) 
  Lemma term_substitutivity': 
    forall tE E0 tE0 ds Eds A,
      wide_typings E0 tE0 ds (imgs tE) A ->
      env_zip tE ds Eds ->
      (forall EE tEE e t A', 
         typing EE tEE e t A' -> tEE = tE -> EE = E0 -> A' = A ->
         wide_typing E0 tE0 (subst_exp Eds e) t A') /\
      (forall EE tEE e t A', 
         wide_typing EE tEE e t A' -> tEE = tE -> EE = E0 -> A' = A ->
         wide_typing E0 tE0 (subst_exp Eds e) t A') /\
      (forall EE tEE es ts A', 
         wide_typings EE tEE es ts A' -> tEE = tE -> EE = E0 -> A = A' ->
         wide_typings E0 tE0 (List.map (subst_exp Eds) es) ts A').
  Proof.
    intros tE E0 tE0 ds Eds A Hb Hz.
    apply typings_mutind; 
      intros;
      subst;
      simpl;
      eauto.
        destruct (binds_zip E0 tE tE0 ds Eds x t A);
          eauto.
        apply binds_implies_get in H2.
        rewrite H2.
        assumption.
      assert (H5' := H5 eq_refl eq_refl eq_refl); clear H5.
      inversion H5'; subst.
      destruct B.
              inversion H3; subst.
              inversion H1; subst.
              eauto.
            inversion H3; subst.
            assert (Hs := sub_t_x _ _ _ _ H7 eq_refl).
            subst.
            inversion H1; subst.
              inversion H1.
              inversion H9.
            apply (wt_sub E0 tE0 _ t t A H); eauto.
          inversion H1; subst.
          inversion H3; subst.
            assert (Hs := sub_t_nested _ _ _ H7 (tin3 s0)).
            subst.
            eauto.
          assert (Hs := sub_t_nested _ _ _ H7 (tin1 s s0)).
          subst.
          eauto.
        inversion H3; subst.
          inversion H.
        assert (Hs := sub_t_nested _ _ _ H7 (tin2 t1 s)).
        subst.
        apply (wt_sub E0 tE0 _ t t A H); eauto.
      inversion H3; subst.
      inversion H.
    assert (H1' := H1 eq_refl eq_refl eq_refl); clear H1.
    inversion H1'; subst.
    assert (Hs := s_trans _ _ _ _ H4 H2).
    apply (wt_sub _ _ _ _ _ _ H1 H3 Hs).
  Qed.

  Lemma term_substitutivity: 
    forall tE tE0 E0 e t ds Eds A,
      wide_typing E0 tE e t A ->
      wide_typings E0 tE0 ds (imgs tE) A ->
      env_zip tE ds Eds ->
      wide_typing E0 tE0 (subst_exp Eds e) t A.
  Proof.
    intros.
    destruct (term_substitutivity' tE E0 tE0 ds Eds A H0 H1)
      as [_ [Hsub _]].
    eapply Hsub; eauto.
  Qed.  

  Hint Resolve term_substitutivity.

Fact eval_at_fun:
  forall t A T T',
    eval_at (t,A) T ->
    eval_at (t,A) T' ->
    T = T'.
Proof.
  intros.
  destruct t; 
    destruct A;
    simpl;
    inversion H;
    inversion H0;
    subst; eauto.
Qed.

Hint Resolve eval_at_fun.

Fact binds_zip':
  forall E0 E tE0 ds Eds v t T T0 ts A,
    typeis_qcname A ->
    eval_ats (imgs E) T0 ts ->
    wide_typings E0 tE0 ds ts A ->
    env_zip E ds Eds ->
    binds v T E ->
    eval_at (T,T0) t ->
    (exists2 e, binds v e Eds & wide_typing E0 tE0 e t A).
Proof.
  intros E0 E.
  induction E; 
    intros; 
    [ | destruct a as (a0,t0)]; inversion H3.
    inversion H2.
    subst. 
    inversion H1.
    subst.
    destruct (v == a0).
      subst injections.
      exists b.
        apply binds_first.
      inversion H0; subst.
      assert (t = t1) by (eapply eval_at_fun; eassumption). 
      subst.
      assumption.
    assert (binds v T E).
      unfold binds.
      assumption.
    inversion H0; subst.
    destruct (IHE _ _ _ _ t _ _ _ _ H H17 H12 H11 H5).
    eauto.
  eauto.
Qed.

Hint Resolve binds_zip'.

Inductive inheritance (env:benv) : type -> type -> Prop :=
| inh_top : forall C D,
    sub env (t_C C) (t_C D) ->
    inheritance env (t_C C) (t_C D)
| inh_nested : forall C D E t tenv m e f,
    sub env (t_C C) (t_C D) ->
    (method m (t_CdotC D E) env t tenv e \/ field (t_CdotC D E) f t) ->
    inheritance env (t_CdotC C E) (t_CdotC D E)
| inh_tt : forall C E,
    inheritance env (t_CdotC C E) (t_dotC E).

Hint Constructors inheritance.

(*
Inductive inheritance' (env:benv) : type -> type -> Prop :=
| inh_top : forall C D,
    sub env (t_C C) (t_C D) ->
    inheritance env (t_C C) (t_C D)
| inh_nested : forall C D E t tenv m e f T,
    sub env (t_C C) (t_C D) ->
    (method m (t_CdotC D E) env t tenv e \/ 
     field (t_CdotC D E) f T) ->
    inheritance env (t_CdotC C E) (t_CdotC D E)
| inh_tt : forall C E,
    inheritance env (t_CdotC C E) (t_dotC E).
*)

Lemma method_implies_typing'':
  forall m t E t0 tE e,
    method m t E t0 tE e ->
    exists t' A, 
      inheritance E t t' /\
      thistype A t' /\
      wide_typing E ((this,t')::tE) e t0 A.
Proof.
  intros m t E t0 tE e H.
  induction H;
    intros;
    subst.
          assert (ok_meth env t m tenv e (t_C C)); eauto.
          unfold ok_meth in H1.
          destruct H1 as [B [H3 [H2 _]]].
          inversion H3; subst.
          exists (t_C C), (t_C C).
          split; eauto.
        destruct IHmethod as [t' [A [IH1 [IH2 IH3]]]].
        exists t', A.
        split.
          inversion IH1; subst.
          apply inh_top.
          apply s_class with (env:=env) in H.
          eauto.
        split.
          inversion IH2; subst.
          eauto.
          apply s_class with (env:=env) in H.
          eauto.
        assumption.
      assert (ok_meth env t m tenv e (t_CdotC C E)); eauto.
      unfold ok_meth in H2.
      destruct H2 as [B [H3 [H2 _]]].
      inversion H3; subst.
      exists (t_dotC E), (t_CdotC C E).
      split;
        eauto.
    destruct IHmethod as [t' [A [IH1 [IH2 IH3]]]].
    exists t', A.
    inversion IH1; subst.
      inversion IH2; subst.
    split; eauto.
  destruct IHmethod as [t' [A [IH1 [IH2 IH3]]]].
  exists t', A.
  inversion IH1; subst.
    inversion IH2; subst.
  split; eauto.
Qed.

Hint Resolve method_implies_typing''.
    
Lemma nil_imgs:
  forall (XPs:tenv),
    nil = imgs XPs ->
    XPs = nil.
Proof.
  intros.
  induction XPs.
  reflexivity.
  inversion H.
Qed.

Hint Resolve nil_imgs.
  
Lemma env_zip_equality:
  forall (XPs:tenv) (XCs:benv) XTs iXPs,
    env_zip XCs iXPs XTs ->
    keys XPs = keys XCs ->
    iXPs = (imgs XPs) ->
    XPs = XTs.
Proof.
  intros XPs XCs XTs iXPs H.
  revert XPs.
  induction H;
    intros.
    apply nil_imgs.
    assumption.    
  inversion H0.
  destruct XPs.
    inversion H1.
  rewrite (IHenv_zip XPs).
      destruct p.
      inversion H0; subst.
      inversion H1; subst.
      reflexivity.
    inversion H3; subst.
    reflexivity.
  inversion H1; subst.
  reflexivity.
Qed.

Hint Resolve env_zip_equality.

Lemma imgs_list_app:
  forall (T:Type) (x:atom) (y:T) l,
    imgs ((x,y) :: l) = y :: (imgs l).
Proof.
  intros.
  eauto.
Qed.

Hint Resolve imgs_list_app.

(** subst_type auxiliary lemmas *)

Lemma subst_type_C:
  forall XTs C,
    subst_type XTs (t_C C) = t_C C.
Proof.
  intros.
  induction XTs.
    unfold subst_type.
    reflexivity.
  simpl.
  unfold subst_type'.
  destruct a; intros;
    destruct t0; intros;
    assumption.
Qed.

Hint Resolve subst_type_C.

Lemma subst_type_CdotC:
  forall XTs C D,
    subst_type XTs (t_CdotC C D) = t_CdotC C D.
Proof.
  intros.
  induction XTs.
    unfold subst_type.
    reflexivity.
  simpl.
  unfold subst_type'.
  destruct a; intros;
    destruct t0; intros;
    assumption.
Qed.

Hint Resolve subst_type_CdotC.

Lemma subst_type_dotC:
  forall XTs C,
    subst_type XTs (t_dotC C) = t_dotC C.
Proof.
  intros.
  induction XTs.
    unfold subst_type.
    reflexivity.
  simpl.
  unfold subst_type'.
  destruct a; intros;
    destruct t0; intros;
    assumption.
Qed.

Hint Resolve subst_type_dotC.

Lemma subst_type_implies_binds:
  forall XTs X C,
    subst_type XTs (t_X X) = t_C C ->
    ok XTs ->
    binds X (t_C C) XTs.
Proof.
  intros.
  induction XTs.
    inversion H.
    destruct a.
  case (t == X);
    intro.
    subst.
    inversion H; subst.
    inversion H0; subst.
    destruct t0.
            rewrite eq_atom_true in *.
            rewrite H2.
            rewrite subst_type_C in H2.
            subst injections.
            apply binds_first.
          assert (IH := IHXTs H2 H4).
          exfalso.
          apply (binds_nobinds IH H6).
        assert (IH := IHXTs H2 H4).
        exfalso.
        apply (binds_nobinds IH H6).
      assert (IH := IHXTs H2 H4).
      exfalso.
      apply (binds_nobinds IH H6).
    assert (IH := IHXTs H2 H4).
    exfalso.
    apply (binds_nobinds IH H6).
  apply binds_other.
    apply IHXTs.
      simpl in H.
      destruct t0; eauto.
      rewrite eq_atom_false in H.
        assumption.
      assumption.
    inversion H0; subst.
    assumption.
  assumption.
Qed.

Hint Resolve subst_type_implies_binds.

Lemma subst_ntype_implies_binds:
  forall XTs X C D,
    subst_type XTs (t_XdotC X D) = t_CdotC C D ->
    ok XTs ->
    binds X (t_C C) XTs.
Proof.
  intros.
  induction XTs.
    inversion H.
    destruct a.
  case (t == X);
    intro.
    subst.
    inversion H; subst.
    inversion H0; subst.
    destruct t0.
            rewrite eq_atom_true in *.
            rewrite subst_type_CdotC in H2.
            subst injections.
            apply binds_first.
          assert (IH := IHXTs H2 H4).
          exfalso.
          apply (binds_nobinds IH H6).
        assert (IH := IHXTs H2 H4).
        exfalso.
        apply (binds_nobinds IH H6).
      assert (IH := IHXTs H2 H4).
      exfalso.
      apply (binds_nobinds IH H6).
    assert (IH := IHXTs H2 H4).
    exfalso.
    apply (binds_nobinds IH H6).
  apply binds_other.
    apply IHXTs.
      simpl in H.
      destruct t0; eauto.
      rewrite eq_atom_false in H.
        assumption.
      assumption.
    inversion H0; subst.
    assumption.
  assumption.
Qed.

Hint Resolve subst_ntype_implies_binds.

Lemma subst_type_X:
  forall XTs X,
    ok XTs ->
    subst_type XTs (t_X X) = t_X X \/
    exists C, subst_type XTs (t_X X) = t_C C.
Proof.
  intros.
  induction XTs.
    left.
    unfold subst_type.
    reflexivity.
  destruct a.
  inversion H; subst.
  destruct IHXTs.
      assumption.
    destruct t; intros;
      eauto.
    destruct (type_dec (t_X a) (t_X X)).
      subst injections.
      right.
      exists s.
      simpl.
      rewrite eq_atom_true.
      apply subst_type_C.
    left.
    simpl.
    rewrite eq_atom_false.
      assumption.
    unfold not in *.
    intro.
    apply H1.
    subst; reflexivity.
  destruct H0 as [C H0].
  right.
  exists C.
  assert (Hst := subst_type_implies_binds _ _ _ H0 H2).
  simpl.
  assert (a <> X).
    unfold not.
    intro.
    subst.
    apply (binds_nobinds Hst H4).
  destruct t; eauto.
  rewrite eq_atom_false;
    assumption.
Qed.

Hint Resolve subst_type_X.

Lemma subst_type_XdotC:
  forall XTs X D,
    ok XTs ->
    subst_type XTs (t_XdotC X D) = t_XdotC X D \/
    exists C, subst_type XTs (t_XdotC X D) = t_CdotC C D.
Proof.
  intros.
  induction XTs.
    left.
    unfold subst_type.
    reflexivity.
  destruct a.
  inversion H; subst.
  destruct IHXTs.
      assumption.
    destruct t; intros;
      eauto.
    destruct (type_dec (t_X a) (t_X X)).
      subst injections.
      right.
      exists s.
      simpl.
      rewrite eq_atom_true.
      apply subst_type_CdotC.
    left.
    simpl.
    rewrite eq_atom_false.
      assumption.
    unfold not in *.
    intro.
    apply H1.
    subst; reflexivity.
  destruct H0 as [C H0].
  right.
  exists C.
  assert (Hst := subst_ntype_implies_binds _ _ _ _ H0 H2).
  simpl.
  assert (a <> X).
    unfold not.
    intro.
    subst.
    apply (binds_nobinds Hst H4).
  destruct t; eauto.
  rewrite eq_atom_false;
    assumption.
Qed.

Hint Resolve subst_type_XdotC.

Lemma subst_type_unfold:
  forall XTs t ts,
    subst_types XTs (t :: ts) = 
    subst_type XTs t :: subst_types XTs ts.
Proof.
  intros.
  unfold subst_types.
  unfold List.map.
  reflexivity.
Qed.

Hint Resolve subst_type_unfold.

Lemma eval_at_top:
  forall S C T,
    eval_at (S, t_C C) T ->
    S = T.
Proof.
  intros.
  destruct S;
    inversion H; subst;
    eauto.
Qed.

Hint Resolve eval_at_top.

Lemma eval_ats_top:
  forall S C c T,
    eval_ats S c T ->
    c = t_C C ->
    S = T.
Proof.
  intros.
  generalize dependent C.
  induction H;
    intros; subst.
  reflexivity.
  apply eval_at_top in H.
  subst.
  rewrite (IHeval_ats C eq_refl).
  reflexivity.
Qed.

Hint Resolve eval_ats_top.
  
Lemma get_weak:
  forall x p (E:tenv),
    get x (p :: E) = None ->
    get x E = None.
Proof.
  intros.
  destruct p.
  inversion H.
  case (x == v).
    intro.
    subst.
    rewrite eq_atom_true in H1.
    inversion H1.
  intro.
  reflexivity.
Qed.

Lemma list_type_dec:
  forall (l l':list type),
    l = l' \/ l <> l'.
Proof.
  intro.
  induction l;
    intros;
    destruct l'.
        left. reflexivity.
      right; unfold not; intros; inversion H.
    right; unfold not; intros; inversion H.
  destruct (IHl l').
    subst.
    destruct (type_dec a t).
      subst.
      left. reflexivity.
    right. unfold not in *. intros. apply H. 
    inversion H0; subst. reflexivity.
  right. unfold not in *. intros. apply H. 
  inversion H0; subst. reflexivity.
Qed.

Lemma exp_dec_implies_list_exp_dec:
  forall es,
    (forall e' : exp, 
       (e' \in es) -> 
       forall e0 : exp, 
         e' = e0 \/ e' <> e0) ->
    forall es', es = es' \/ es <> es'.
Proof.
  intro.
  induction es; intros.
    destruct es'.
      left. reflexivity.
    right. unfold not. intros.
    inversion H0.
  destruct es'.
    right. unfold not. intros. inversion H0.
  assert (a = e \/ a <> e).
    apply H.
    unfold In.
    left. reflexivity.
  destruct H0.
    subst.
    assert (es = es' \/ es <> es').
      apply IHes.
      intros.
      apply H.
      unfold In in *.
      right. assumption.
    destruct H0.
      subst.
      left. reflexivity.
    right.
    unfold not in *.
    intro.
    apply H0.
    inversion H1; subst.
    reflexivity.
  right. unfold not in *.
  intros. apply H0. inversion H1; subst.
  reflexivity.
Qed. 

Lemma exp_dec:
  forall (e e0:exp),
    e = e0 \/ e <> e0.
Proof.
  intro;
  induction e using exp_ind2;
  intro;
  destruct e0.
    case (v == v0); intros; subst; eauto.
    unfold not in *; right; intro; apply n; subst injections; eauto.
    unfold not in *; right; intro; inversion H.
    unfold not in *; right; intro; inversion H.
    unfold not in *; right; intro; inversion H.
    unfold not in *; right; intro; inversion H.
    destruct (IHe e0).
      subst. case (f == f0). intro. subst. left. reflexivity.
      intro. right. unfold not in *. intro. apply n. 
      subst injections. reflexivity.
      right. unfold not in *. intro. apply H. 
      subst injections. reflexivity.
    unfold not in *; right; intro; inversion H.  
    unfold not in *; right; intro; inversion H.
    unfold not in *; right; intro; inversion H0. 
    unfold not in *; right; intro; inversion H0. 
    destruct (IHe e0). subst. 
      case (m == m0). intro. subst.
        destruct (list_type_dec l l1). subst.
          destruct (exp_dec_implies_list_exp_dec _ H l2).
            subst.
            left; reflexivity.
          right. unfold not in *. intros.
          apply H0. inversion H1. reflexivity.
        right. unfold not in *. intros.
        apply H0. inversion H1. reflexivity.
      right. unfold not in *. intros.
      apply n. inversion H0. reflexivity.
    right. unfold not in *. intro.
    apply H0. inversion H1; subst. reflexivity.
    unfold not in *; right; intro; inversion H0.  
    unfold not in *; right; intro; inversion H0.  
    unfold not in *; right; intro; inversion H0.  
    unfold not in *; right; intro; inversion H0.  
  destruct (type_dec t t0).
    subst.
    destruct (exp_dec_implies_list_exp_dec _ H l0).
      subst. left. reflexivity.
    right. unfold not in *. intros. apply H0. 
    inversion H1; subst. reflexivity.
  right. unfold not in *. intros. apply H0. 
  inversion H1; subst. reflexivity.
Qed.

Lemma keys_list_app:
  forall x (a:type) l,
    keys ((x,a) :: l) = x :: keys l.
Proof.
  intros.
  unfold keys.
  eauto.
Qed.

Lemma keys_l_nil:
  forall l:tenv,
    keys l = nil ->
    l = nil.
Proof.
  intros.
  induction l.
  reflexivity.
  destruct a.
  rewrite keys_list_app in H.
  inversion H.
Qed.

Lemma env_zip_nobinds:
  forall aenv benv (bs:list type) y x (a b:type),
    env_zip aenv bs benv ->
    no_binds y ((x,a) :: aenv) ->
    no_binds y ((x,b) :: benv).
Proof.
  intros aenv benv bs y x a b H.
  revert y x a b.
  induction H; intros.
    case (y == x).
      intro.
      subst.
      inversion H.
      rewrite eq_atom_true in H1.
      inversion H1.
    intro.
    unfold no_binds.
    unfold get.
    rewrite eq_atom_false; eauto.
  case (y == x0).
    intro.
    subst.
    inversion H0; subst.
    rewrite eq_atom_true in H2.
    inversion H2.
  intro.
  apply nobinds_cons; eauto.
  inversion H0; subst.
  rewrite eq_atom_false in H2; eauto.
Qed.

Lemma ok_env_zip:
  forall xTs S T T' xts ts,
    eval_ats (imgs xTs) S ts ->
    env_zip xTs ts xts ->
    ok ((this, T) :: xTs) ->
    ok ((this, T') :: xts).    
Proof.
  intros xTs S T T' xts ts H0 H H1.
  revert H0 H1.
  revert S T T'.
  induction H; intros; subst.
    apply ok_cons.
      apply ok_nil.    
    unfold no_binds; eauto.
  rewrite imgs_list_app in H0.
  inversion H0; subst.
  apply ok_cons.
    apply ok_cons.
      inversion H1; subst.
      inversion H4; subst.
      apply ok_cons with (x:=this) (v:=T) in H5.
        assert (IH := IHenv_zip S T T' H8 H5).
        inversion IH; subst.
        assumption.
      case (this == x).
        intro.
        subst.
        assumption.
      intro.
      unfold no_binds.
      inversion H7; subst.
      rewrite eq_atom_false in *; eauto.
    inversion H1; subst.
    inversion H4; subst.
    destruct benv.
      unfold no_binds; eauto.
    destruct aenv.
    inversion H; subst.
    destruct p.
    inversion H; subst.
    apply (env_zip_nobinds _ _ _ _ _ _ _ H11 H10).
  inversion H1; subst.
  apply (env_zip_nobinds _ _ _ _ _ _ _ H H7).
Qed.

Lemma sub_subst_type:
  forall E E' C c U XTs, 
    C = t_C c ->
    sub E C U ->
    sub E' C (subst_type XTs U).
Proof.
  intros E E' C c U XTs H0 H.
  revert H0.
  revert E' c XTs.
  induction  H; intros; subst.
          rewrite subst_type_C.
          apply s_refl.
        inversion H0.
      rewrite subst_type_C.
      apply s_object.
    destruct (sub_tlc_implies_tlc _ _ _ _ H eq_refl).
    subst.
    destruct (sub_tlc_implies_tlc _ _ _ _ H0 eq_refl).
    subst.
    assert (IH2 := IHsub2 E' x XTs eq_refl).
    assert (IH1 := IHsub1 E' c XTs eq_refl).
    rewrite subst_type_C in IH1.    
    apply (s_trans _ _ _ _ IH1 IH2).
  subst injections.
  rewrite subst_type_C.
  apply (s_class _ _ _ _ _ _ _ H).
Qed.

Lemma binds_env_zip':
  forall x t xTs xts S ts t',
    binds x t xTs ->
    eval_ats (imgs xTs) S ts ->
    eval_at (t, S) t' ->
    env_zip xTs ts xts ->
    binds x t' xts.
Proof.
  intros x t xTs xts S ts t' H1 H0 H2 H.
  revert H2 H1 H0.
  revert x t t' S.
  induction H; intros; subst.
    inversion H1.
  inversion H0; subst.
  case (x == x0).
    intro.
    subst.
    inversion H1; subst.
    rewrite eq_atom_true in H4.
    subst injections.
    assert (He := eval_at_fun _ _ _ _ H2 H7).
    subst.
    apply binds_first.
  intro.
  apply binds_other with (2:=n).
  inversion H1; subst.
  rewrite eq_atom_false in H4; eauto.
Qed.

Lemma binds_env_zip:
  forall x t xTs xts XTs ts,
    binds x t xTs ->
    ts = subst_types XTs (imgs xTs) ->
    env_zip xTs ts xts ->
    binds x (subst_type XTs t) xts.
Proof.
  intros x t xTs xts XTs ts H1 H0 H.
  revert H1 H0.
  revert x t XTs.
  induction H; intros; subst.
    inversion H1.
  inversion H0; subst.
  case (x == x0).
    intro.
    subst.
    inversion H1; subst.
    rewrite eq_atom_true in H3.
    subst injections.
    apply binds_first.
  intro.
  apply binds_other with (2:=n).
  apply IHenv_zip.
  inversion H1; subst.
  rewrite eq_atom_false in H3.
  unfold binds.
  assumption.
  unfold not in *.
  intro. apply n. symmetry. assumption.
  reflexivity.
Qed.

(* (** ** Type substitutivity lemma *) 
Lemma type_substitutivity': 
  forall XCs t' C m U xTs b XTs t0 xts A E0 tE0 tE' es' ts',
    inheritance XCs (t_C C) t' ->
    wide_typing XCs ((this, t') :: xTs) b U t' ->
    method m (t_C C) XCs U xTs b -> 
    subs E0 (imgs XTs) (imgs XCs) ->
    eval_at (subst_type XTs U, t_C C) t0 -> 
    eval_ats (subst_types XTs (imgs xTs)) (t_C C) ts' ->
    env_zip xTs ts' xts ->
    wide_typings E0 tE' es' ts' A ->
    ((this,t_C C)::xts) = tE0 -> 
    (forall E tE e t A',
       typing E tE e t A' -> 
       tE = ((this, t') :: xTs) -> A' = A -> e = b -> t = U ->
       wide_typing E0 tE0 (subst_type_exp XTs e) t0 A') /\
    (forall E tE e t A',
       wide_typing E tE e t A' ->
       tE = ((this, t') :: xTs) -> A' = A -> e = b -> t = U ->
       wide_typing E0 tE0 (subst_type_exp XTs e) t0 A') /\
    (forall E tE es ts A',
       wide_typings E tE es ts A' ->
       tE = ((this, t') :: xTs) -> A' = A -> 
       wide_typings E0 tE0 (List.map (subst_type_exp XTs) es) ts A').
Proof.
  intros XCs t' C m U xTs b XTs t0 xts A E0 tE0 tE' es' ts' 
         H H0 H1 H2 H3 H4 H5 H6 H7.
  assert (Hat := eval_at_top _ _ _ H3).
  assert (Hats := eval_ats_top _ C _ _ H4 eq_refl).
  assert (HA : typeis_qcname A).
    inversion H6; subst; eauto.
  subst. 
  apply typings_mutind;
    intros;
    subst;
    simpl.
Admitted.
  
Lemma type_substitutivity: 
  forall XCs C xTs b U A m t0 E XTs t' xts ts tE es,
    inheritance XCs (t_C C) t' ->
    wide_typing XCs ((this,t')::xTs) b U t' ->
    method m (t_C C) XCs U xTs b ->
    subs E (imgs XTs) (imgs XCs) ->
    eval_at (subst_type XTs U, (t_C C)) t0 ->
    eval_ats (subst_types XTs (imgs xTs)) (t_C C) ts ->
    env_zip xTs ts xts ->
    wide_typings E tE es ts A ->
    wide_typing E ((this,t_C C)::xts) (subst_type_exp XTs b) t0 A.
Proof.
  intros.
  destruct (type_substitutivity' XCs t' C m U xTs b XTs t0 xts 
                                 t' E ((this,t_C C)::xts) tE es ts)
    as [_ [Hsub _]]; eauto.
Admitted. *)

Lemma exists_env_zip:
  forall (XTs xTs:tenv) (ts:list type) C,
    eval_ats (subst_types XTs (imgs xTs)) (t_C C) ts ->
    exists xts, env_zip xTs ts xts.
Proof.
  intros XTs xTs.
  revert XTs.
  induction xTs;
    intros.
    inversion H; subst.
    eauto.
  destruct ts.
    inversion H.
  inversion H; subst.
  destruct (IHxTs XTs ts C H6).
  destruct a.
  exists ((v,t)::x).
  apply z_cons.
  assumption.
Qed.

Hint Resolve exists_env_zip.

Lemma exists_env_zip':
  forall (XTs xTs:tenv) (ts:list type) C D,
    eval_ats (subst_types XTs (imgs xTs)) (t_CdotC C D) ts ->
    exists xts, env_zip xTs ts xts.
Proof.
  intros XTs xTs.
  revert XTs.
  induction xTs;
    intros.
    inversion H; subst.
    eauto.
  destruct ts.
    inversion H.
  inversion H; subst.
  destruct (IHxTs XTs ts C D H6).
  destruct a.
  exists ((v,t)::x).
  apply z_cons.
  assumption.
Qed.

Hint Resolve exists_env_zip'.

Lemma exists_env_zip_method:
  forall E es ts A XPs xTs C,
    wide_typings E nil es ts A ->
    eval_ats (subst_types XPs (imgs xTs)) C ts ->
    exists ves, env_zip xTs es ves.
Proof.
  intros E es ts A XPs xTs.
  revert E es ts A XPs.
  induction xTs;
    intros.
    inversion H0; subst.
    inversion H; subst.
    exists nil.
    eauto.
  destruct es.
    inversion H; subst.
    inversion H0.
  destruct ts.
    inversion H.
  destruct (IHxTs E es ts A XPs C).
      inversion H; subst.
      assumption.
    inversion H0; subst.
    assumption.
  destruct a.
  exists ((a,e)::x).
  apply z_cons.
  assumption.
Qed.

Lemma nil_imgs_l:
  forall (A:Type) (l:list (atom*A)),
    nil = imgs l ->
    l = nil.
Proof.
  intros.
  induction l.
    reflexivity.
  inversion H.
Qed.

Lemma imgs_l_nil:
  forall (A:Type) (l:list (atom*A)),
    imgs l = nil ->
    l = nil.
Proof.
  intros.
  induction l.
    reflexivity.
  inversion H.
Qed.

Lemma exists_env_zip_fields:
  forall C (x:fenv) E ts A (es:list exp),
    wide_typings E nil es ts A ->
    eval_ats (imgs x) C ts ->
    exists xes, env_zip x es xes. 
Proof.
  intros C x.
  revert C.
  induction x;
    intros.
    inversion H0; subst.
    inversion H; subst.
    eauto.
  destruct es.
    inversion H; subst.
    inversion H0.
  destruct ts.
    inversion H.
  destruct (IHx C E ts A es).
      inversion H; subst.
      assumption.
    inversion H0; subst.
    assumption.
  destruct a.
  exists ((f,e)::x0).
  apply z_cons; eauto.
Qed.

Lemma exists_env_zip_subs:
  forall E XPs XCs,
    subs E (imgs XPs) (imgs XCs) ->
    exists XTs, env_zip XCs (imgs XPs) XTs. 
Proof.
  intros E XPs.
  revert E.
  induction XPs;
    intros.
    inversion H; subst.
    apply nil_imgs_l in H1.
    subst.
    assert (H1 : imgs (nil:list (atom*type)) = nil).
      eauto.
    rewrite H1.
    eauto.
  destruct XCs.
    inversion H.
  destruct a.
  destruct p.
  rewrite imgs_list_app in *.
  rewrite imgs_list_app in H.
  destruct (IHXPs E XCs).
    inversion H; subst.
    assumption.
  exists ((a0,t)::x).
  apply z_cons.
  assumption.
Qed.
                                           
Lemma exists_binds:
  forall f (T:type) x (es:list exp) xes,
    binds f T x ->
    env_zip x es xes ->
    exists e, binds f e xes. 
Proof.
  intros f T x es xes H0 H.
  revert H0.
  revert f T.
  induction H; intros.
    inversion H0.
  case (f == x).
    intro.
    subst.
    inversion H0; subst.
    exists b. apply binds_first.
  intro.
  destruct (IHenv_zip f T).
    inversion H0.
    rewrite eq_atom_false in H2.
      unfold binds.
      assumption.
    assumption.
  exists x0.
  apply binds_other.
    assumption.
  unfold not in *.
  intro.
  apply n.
  symmetry.
  assumption.
Qed.

Lemma env_zip_zip:
  forall (xTs xts:tenv) (es:list exp) ves ts,
    env_zip xTs es ves -> 
    env_zip xTs ts xts ->
    env_zip xts es ves.
Proof.
  intros.
  revert H0.
  revert xts ts.
  induction H;
    intros.
    inversion H0; subst.
    eauto.
  destruct xts.
    inversion H0.
  destruct p.
  inversion H0; subst.
  apply z_cons.
  apply (IHenv_zip xts bs0).
  assumption.
Qed.

Hint Resolve env_zip_zip.

Lemma env_zip_imgs:
  forall (xTs:tenv) (ts:list type) xts,
    env_zip xTs ts xts ->
    imgs xts = ts.
Proof.
  intros.
  induction H.
    eauto.
  rewrite imgs_list_app.
  rewrite IHenv_zip.
  reflexivity.
Qed.
                                         
Hint Resolve env_zip_imgs.

Lemma subst_types_nil:
  forall ts,
    subst_types nil ts = ts.
Proof.
  intros.
  unfold subst_types.
  unfold subst_type.
  apply map_id.
Qed.

Lemma subst_type_exp_field:
  forall e f, 
    subst_type_exp nil (e_field e f) = 
    e_field (subst_type_exp nil e) f.
Proof.
  intros.
  unfold subst_type_exp.
  reflexivity.
Qed.

Lemma subst_type_exp_meth:
  forall e m Ps es, 
    subst_type_exp nil (e_meth e m Ps es) = 
    e_meth (subst_type_exp nil e) m (subst_types nil Ps)
           (List.map (subst_type_exp nil) es).
Proof.
  intros.
  unfold subst_type_exp.
  reflexivity.
Qed.

Lemma subst_type_exp_new:
  forall C es, 
    subst_type_exp nil (e_new C es) = 
    e_new (subst_type nil C) (List.map (subst_type_exp nil) es).
Proof.
  intros.
  unfold subst_type_exp.
  reflexivity.
Qed.

Lemma map_subst_type_cons:
  forall a l,
    List.map (subst_type_exp nil) (a :: l) = 
    subst_type_exp nil a :: (List.map (subst_type_exp nil) l).
Proof.
  intros.
  unfold List.map.
  reflexivity.
Qed.

Lemma subst_type_exp_list:
  forall l,
  (forall e' : exp, e' \in l -> subst_type_exp nil e' = e') ->
  List.map (subst_type_exp nil) l = l.
Proof.
  intro l.
  induction l; intros.
    eauto.
  rewrite map_subst_type_cons.
  assert (subst_type_exp nil a = a).
    apply H.
    unfold In.
    left.
    reflexivity.
  rewrite H0.
  rewrite IHl.
    reflexivity.
  intros.
  destruct (exp_dec e' a).
    rewrite H2.
    assumption.
  apply H.
  unfold In.
  right.
  assumption.
Qed.

Lemma subst_type_exp_nil:
  forall e,
    subst_type_exp nil e = e.
Proof.
  intros.
  induction e using exp_ind2; eauto.
      rewrite subst_type_exp_field.
      rewrite IHe.
      reflexivity.
    rewrite subst_type_exp_meth.
    rewrite IHe.
    unfold subst_types.
    unfold subst_type.
    rewrite map_id.
    rewrite subst_type_exp_list.
      reflexivity.
    assumption.
  rewrite subst_type_exp_new.
  unfold subst_type.
  rewrite subst_type_exp_list.
    reflexivity.
  assumption.
Qed.

Lemma eval_at_sub:
  forall T C0 t0 t,
    eval_at (T, C0) t ->
    sub nil t0 C0 ->
    eval_at (T, t0) t.
Proof.
  intros T C0 t0 t H0 H.
  revert H0. revert T t.
  induction H; intros; eauto.
      assert (He := eval_at_top _ _ _ H0).
      subst.
      destruct t; eauto.
      inversion H0.
    assert (He := eval_at_top _ _ _ H0).
    subst.
    destruct t; eauto.
    inversion H0.    
  assert (He := eval_at_top _ _ _ H0).
  subst.
  destruct t; eauto.
  inversion H0.    
Qed.  

Lemma eval_ats_sub:
  forall T C0 t0 t,
    eval_ats T C0 t ->
    sub nil t0 C0 ->
    eval_ats T t0 t.
Proof.
  intros T C0 t0 t H H0.
  revert H0. revert t0.
  induction H; intros; eauto.
  apply ca_cons.
    apply (eval_at_sub _ _ _ _ H H1).
  apply IHeval_ats.
  assumption.
Qed.  

Lemma sub_nil_var:
  forall t X T, 
    sub nil X T ->
    X = t_X t ->
    X <> T ->
    T <> t_C Object ->
    False.
Proof.
  intros t X T H.
  revert t.
  induction H; intros; subst; eauto.
  inversion H.
  destruct (type_dec (t_X t) T).
    subst.
    eauto.
  assert (T <> t_C Object).
    unfold not. intro. subst.
    assert (Hs := sub_object_object _ _ _ H0 eq_refl).
    subst.
    unfold not in H3. apply H3. reflexivity.
  apply (IHsub1 _ eq_refl H1 H4).
  inversion H0.
Qed.

Lemma sub_nil_var_nested:
  forall t C X T, 
    sub nil X T ->
    X = t_XdotC t C ->
    X <> T ->
    T <> t_C Object ->
    False.
Proof.
  intros t C X T H.
  revert t C.
  induction H; intros; subst; eauto.
  inversion H.
  destruct (type_dec (t_XdotC t C) T).
    subst.
    eauto.
  assert (T <> t_C Object).
    unfold not. intro. subst.
    assert (Hs := sub_object_object _ _ _ H0 eq_refl).
    subst.
    unfold not in H3. apply H3. reflexivity.
  apply (IHsub1 _ _ eq_refl H1 H4).
  inversion H0.
Qed.

Lemma field_sub:
  forall C0 f0 T t0 A B C',
    sub nil t0 C0 ->
    eval_at (t0, A) B ->
    eval_bound nil B C' ->
    field C0 f0 T ->
    field C' f0 T.
Proof.
  intros C0 f0 T t0 A B C' H.
  revert f0 T A B C'.
  induction H; intros; eauto.
  destruct T.
                  inversion H; subst.
                  inversion H0; subst.
                  assumption.
                inversion H1.
                inversion H2.
              inversion H; subst.
              inversion H0; subst.
              assumption.
            inversion H1.
            inversion H2.
          inversion H; subst.
              inversion H1.
              inversion H2.
            inversion H1.
            inversion H2.
          inversion H0; subst.
          assumption.
        inversion H.
      inversion H1.
      assert (H3' := f_tobject).
      assert (He := Facts1.fields_fun _ _ _ H2 H3').
      subst.
      inversion H3.
    destruct (type_dec S T).
      subst.
      eauto.
    assert (B = C').
      inversion H2; subst; eauto. 
        inversion H2; subst.
        inversion H9.
      inversion H2; subst.
      inversion H8.
    subst.
    destruct S.
            inversion H1; subst.
            destruct (sub_tlc_implies_tlc _ _ _ _ H eq_refl).
            subst.
            destruct (type_dec (t_C x) U).
              subst.
              assert (eval_at (t_C x, A) (t_C x)).
                eauto.
              assert (eval_bound nil (t_C x) (t_C x)).
                eauto.
              assert (IH2 := IHsub2 _ _ _ _ _ H5 H6 H3).
              eapply IHsub1; eauto.
            assert (U <> t_C Object).
              unfold not. intro. subst.
              inversion H3.
              assert (Hf := f_tobject).
              assert (He := Facts1.fields_fun _ _ _ H6 Hf).
              subst.
              inversion H7.
            destruct (sub_tlc_implies_tlc _ _ _ _ H0 eq_refl).
            subst.              
            inversion H1; subst.
            inversion H2; subst.
            eauto.
          inversion H1; subst.
          inversion H2; subst.
          inversion H5.
        destruct (sub_nested_t _ _ _ H (tin1 s s0)).
          subst.
          unfold not in H4. exfalso. apply H4. reflexivity.
        subst.
        assert (Hs := sub_object_object _ _ _ H0 eq_refl).
        subst.
        inversion H3.
        assert (Hf := f_tobject).
        assert (He := Facts1.fields_fun _ _ _ H5 Hf).
        subst.
        inversion H6.
      inversion H1; subst.
      inversion H2; subst.
      inversion H5.
    destruct (sub_nested_t _ _ _ H (tin3 s)).
      subst.
      unfold not in H4. exfalso. apply H4. reflexivity.
    subst.
    assert (Hs := sub_object_object _ _ _ H0 eq_refl).
    subst.
    inversion H3.
    assert (Hf := f_tobject).
    assert (He := Facts1.fields_fun _ _ _ H5 Hf).
    subst.
    inversion H6.
  inversion H0; subst.
  inversion H1; subst.
  inversion H2.
  assert (Hf := f_tclass _ _ _ _ _ _ _ H H4).
  unfold field.
  exists (x ++ fs).
  eauto.
  apply binds_head.
  assumption.
  Grab Existential Variables.
  apply A.
Qed.

Lemma sub_dot_nested_false:
  forall s t E C D,
    sub nil s t ->
    s = (t_dotC E) ->
    t = (t_CdotC C D) ->
    False.
Proof.
  intros s t E C D H.
  revert E C D.
  induction H; intros; subst.
  inversion H0.
  inversion H0.
  inversion H0.
  assert (Hx := sub_nested_t _ _ _ H (tin3 E)).
  destruct Hx.
    subst.
    apply (IHsub2 E C D eq_refl eq_refl).
  subst.
  inversion H0; subst.
  assert (Hoo := sub_object_object _ _ _ H0 eq_refl).
  inversion Hoo.
  inversion H0.
Qed.

Lemma sub_nested_dot_false:
  forall s t E C D,
    sub nil t s ->
    s = (t_dotC E) ->
    t = (t_CdotC C D) ->
    False.
Proof.
  intros s t E C D H.
  revert E C D.
  induction H; intros; subst.
  inversion H0.
  inversion H0.
  inversion H.
  assert (Hx := sub_nested_t _ _ _ H (tin1 C D)).
  destruct Hx.
    subst.
    apply (IHsub2 E C D eq_refl eq_refl).
  subst.
  inversion H0; subst.
  assert (Hoo := sub_object_object _ _ _ H0 eq_refl).
  inversion Hoo.
  inversion H0.
Qed.

Lemma sub_nested_var_dot_false:
  forall s t E X D,
    sub nil t s ->
    s = (t_dotC E) ->
    t = (t_XdotC X D) ->
    False.
Proof.
  intros s t E X D H.
  revert E X D.
  induction H; intros; subst.
  inversion H0.
  inversion H0.
  inversion H.
  assert (Hx := sub_nested_t _ _ _ H (tin2 X D)).
  destruct Hx.
    subst.
    apply (IHsub2 E X D eq_refl eq_refl).
  subst.
  inversion H0; subst.
  assert (Hoo := sub_object_object _ _ _ H0 eq_refl).
  inversion Hoo.
  inversion H0.
Qed.

Lemma method_benv_nil:
  forall m C XCs t xTs e,
    method m C XCs t xTs e ->
    XCs = nil.
Proof.
  intros.
  assert (Hok : ok_cenv CT). 
    apply H.ok_ct.
  unfold ok_cenv in Hok.
  induction H.  
          assert (ok_tclass' C (D,fs,c,ms,ns)).
            destruct Hok as [Hok Hok'].
            apply binds_forall_class.
              assumption.
            assumption.
          assert (ok_tclass C D fs c ms ns).
            unfold ok_tclass' in H1.
            assumption.
          unfold ok_tclass in H2.
          destruct H2 as [A' [gs [_ [_ [H2 _]]]]].
          assert (ok_meth' (t_C C) m (env,t,tenv,e)).
            apply (binds_forall_method _ _ H2 _ _ H0).
          assert (ok_meth env t m tenv e (t_C C)).
            unfold ok_meth' in H3.
            assumption.
          unfold ok_meth in H4.
          destruct H4 as [B [_ [_ [_ [_ [_ [H4 _]]]]]]].
          assumption.
        assumption.
      assert (ok_tclass' C (D,fs,c,ms,ns)).
        destruct Hok as [Hok Hok'].
        apply binds_forall_class.
          assumption.
        assumption.
      assert (ok_tclass C D fs c ms ns).
        unfold ok_tclass' in H2.
        assumption.
      unfold ok_tclass in H3.
      destruct H3 as [A' [gs [_ [_ [_ [H3 _]]]]]].
      assert (ok_nclass E fs' c' ms' C).
        apply (binds_forall_nclass _ _ H3 _ _ H0).
      unfold ok_nclass in H4.
      destruct H4 as [gs' [_ [_ [_ [_ [_ H4]]]]]].
      assert (ok_meth' (t_CdotC C E) m (env,t,tenv,e)).
        apply (binds_forall_method _ _ H4 _ _ H1).
      assert (ok_meth env t m tenv e (t_CdotC C E)).
        unfold ok_meth' in H5.
        assumption.
      unfold ok_meth in H6.
      destruct H6 as [B [_ [_ [_ [_ [_ [H6 _]]]]]]].
      assumption.
    assumption.
  assumption.
Qed.

Lemma wts_exp_aux:
  forall l C D A ts xts Ds,
    (forall e' U, In e' l ->
     wide_typing nil ((this, D) :: xts) e' U D ->
     wide_typing nil ((this, C) :: xts) e' U A) ->
    typeis_qcname A ->
    Ds = ((this, D) :: xts) ->
    wide_typings nil Ds l ts D ->
    wide_typings nil ((this, C) :: xts) l ts A.
Proof.
  intros l C D A ts xts Ds H H0 H1 H2.
  revert H H0 H1.
  revert C A xts.
  induction H2; intros; subst.
    apply wts_nil; eauto.
    inversion H1; subst.
    eauto.
  apply wts_cons.
      assumption.
    apply IHwide_typings.
      intros.
      apply H1.
        unfold In in *. right. assumption.
      assumption.
    assumption.
    reflexivity.
  apply H1.
    unfold In. left. reflexivity.
  assumption.
Qed.

Lemma exists_eval_at:
  forall t0 A C0,
    sub nil t0 C0 ->
    typeis_qcname C0 ->
    typeis_qcname A ->
    C0 <> t_C Object ->
    exists B, eval_at (t0, A) B.
Proof.
  intros.
  inversion H0; subst.
    destruct t0; eauto.
    apply sub_nested_t in H; eauto.
    destruct H.
      inversion H.
    subst injections.
    contradiction H2. reflexivity.
  destruct t0; eauto.
  exfalso.
  apply (sub_dot_nested_false _ _ _ _ _ H eq_refl eq_refl).
Qed.

Lemma ea_substitutivity_top:
  forall C D b U A xts,
    wide_typing nil ((this, t_C D) :: xts) b U (t_C D) ->
    typeis_qcname A ->
    sub nil (t_C C) (t_C D) ->
    wide_typing nil ((this, t_C C) :: xts) b U A.
Proof.
  intros C D b.
  revert C D.
  induction b using exp_ind2;
    intros.

        inversion H; subst.
        inversion H3; subst.
        case (v == this).
          intro.
          subst.
          inversion H10; subst.
          rewrite eq_atom_true in H8.
          subst injections.
          apply wt_sub with (t:=t_C C); eauto.
          inversion H7; subst.
          apply t_var; eauto.
          apply binds_first.
        intro.
        inversion H10; subst.
        rewrite eq_atom_false in H8; eauto.
        assert (binds v t xts).
          unfold binds.
          assumption.
        apply wt_sub with (t:=t); eauto.
        inversion H7; subst.
        apply t_var; eauto.

      inversion H; subst.
      inversion H3; subst.
      assert (H16' := wt_sub _ _ _ _ _ _ (tiq_C D) H16 (s_refl nil T0)).
      assert (IH := IHb _ _ _ _ _ H16' H0 H1).
      apply wt_sub with (t:=t); eauto.
      apply eval_at_top in H13.
      subst.
      assert (B = C0).
        inversion H9; subst; eauto.
          inversion H5.
        inversion H5.
      subst.
      clear H7; clear H2.
      assert (typeis_qcname C0).
        inversion H8; subst; eauto.
      assert (eval_at (C0, A) C0).
        inversion H2; subst; eauto.
      inversion IH; subst.
      assert (exists B, eval_at (t0, A) B).
        assert (C0 <> t_C Object).
          unfold not.
          intro. subst. inversion H8.
          assert (Hf := f_tobject).
          assert (He := Facts1.fields_fun _ _ _ H12 Hf).
          subst.
          inversion H13.
        apply (exists_eval_at _ _ _ H11 H2 H6 H12).
      destruct H12 as [B H12].
      assert (C0 <> t_C Object).
        unfold not. intro. subst.
        inversion H8.
        assert (Hf := f_tobject).
        apply Facts1.fields_fun with (fs:=x) in Hf.
        subst.
        inversion H14.        
        assumption.
      assert (eval_bound nil B B).
        destruct B; eauto.
            inversion H12; subst.
            exfalso. apply (sub_nil_var _ _ _ H11 eq_refl).
            unfold not. intro. subst. inversion H2.
            unfold not. intro. subst.
            unfold not in H13. apply H13. reflexivity.
          inversion H12; subst.
            inversion H0.            
          exfalso. apply (sub_nil_var_nested _ _ _ _ H11 eq_refl).
          unfold not. intro. subst. inversion H8. inversion H14.
          assumption.
        inversion H12; subst.
        inversion H6.
      assert (field B f0 T).      
        apply (field_sub _ _ _ _ _ _ _ H11 H12 H14 H8).
      assert (eval_at (T, t0) t).
        apply (eval_at_sub _ _ _ _ H10 H11).
      apply (t_field _ _ _ _ _ _ _ _ _ _ H0 H15 H14 H17 H12 H7).

    inversion H0; subst.
    inversion H4; subst.
    assert (H25' := wt_sub _ _ _ _ _ _ (tiq_C D) H25 (s_refl nil T0)).
    assert (IH := IHb _ _ _ _ _ H25' H1 H2).
    apply wt_sub with (t:=t); eauto.
    apply eval_at_top in H22.
    subst.
    assert (B = C0).
      inversion H19; subst; eauto.
        inversion H6.
      inversion H6.
    subst.
    assert (typeis_qcname C0).
      inversion H19; subst; eauto.
    assert (Hm := method_benv_nil _ _ _ _ _ _ H18).
    subst.
    inversion H14; subst.
    rewrite H8 in *.
    apply keys_l_nil in H8.
    subst.
    rewrite subst_types_nil in *.
    unfold subst_type in *.
    clear H14; clear H11; clear H27; clear H3; clear H10; clear H19.
    simpl in *.
    inversion IH; subst.
    assert (exists B, eval_at (t0, A) B).
      assert (C0 <> t_C Object).
        unfold not. intro. subst. 
        assert (Ho := Facts1.obj_nomeths m nil xTs U0 b0).
        unfold not in Ho.
        exfalso. apply Ho. assumption.
      apply (exists_eval_at _ _ _ H8 H6 H3 H9).
    destruct H9 as [B H9].
    assert (C0 <> t_C Object).
      unfold not. intro. subst.
      assert (Hm := Facts1.obj_nomeths m nil xTs U0 b0). 
      unfold not in Hm.
      apply Hm. assumption.
    assert (eval_bound nil B B).
      destruct B; eauto.
          inversion H9; subst.
          exfalso. apply (sub_nil_var _ _ _ H8 eq_refl).
          unfold not. intro. subst. inversion H6.
          assumption.
        inversion H9; subst.
          inversion H1.          
        exfalso. apply (sub_nil_var_nested _ _ _ _ H8 eq_refl).
        unfold not. intro. subst. inversion H6.
        assumption.
      inversion H9; subst.
      inversion H1.
    assert (t0 = B).
      inversion H9; subst; eauto.
        apply sub_nested_t in H8; eauto.
        destruct H8.
          subst.
          inversion H18.
        subst.
        assert (Ho := Facts1.obj_nomeths m nil xTs U0 b0).
        unfold not in Ho.
        exfalso. apply Ho. assumption.
      inversion H1.
    subst.
    assert (Hm := sub_mtype _ _ _ _ _ _ _ _ _ H8 H18 H11).
    destruct Hm as [ue Hm].
    assert (eval_at (U0, B) t).
      apply (eval_at_sub _ _ _ _ H12 H8).
    assert (wide_typings nil ((this, t_C C) :: xts) l0 ts A).
      eapply wts_exp_aux with (D:=t_C D); eauto.
    apply (t_invk _ _ nil U0 B _ ts (imgs xTs) nil nil
                  _ xTs _ _ B B _ _ ue); eauto.
    rewrite subst_types_nil.
    apply (eval_ats_sub _ _ _ _ H13 H8).

  inversion H0; subst.
  inversion H4; subst.
  apply wt_sub with (t:=t0); eauto.
  assert (wide_typings nil ((this,t_C C)::xts) l ts A).
    eapply wts_exp_aux with (D:=t_C D); eauto.
  apply (t_new _ fs _ _ _ _ ts); eauto.
Qed.

Lemma eval_at_binds:
  forall xTs ts xts C D T T' v, 
    env_zip xTs ts xts ->
    eval_ats (imgs xTs) (t_CdotC C D) ts ->
    eval_at (T, t_CdotC C D) T' ->
    binds v T xTs ->
    binds v T' xts.
Proof.
  intros xTs ts xts C D T T' v H.
  revert C D T T' v.
  induction H; intros.
    inversion H1.
  inversion H0; subst.
  case (v == x).
    intro.
    subst.
    inversion H2; subst.
    rewrite eq_atom_true in H4; eauto.
    subst injections.
    inversion H1; subst; inversion H7; subst; apply binds_first.
  intro.
  apply binds_other.
    inversion H2; subst.
    rewrite eq_atom_false in H4; eauto.
  unfold not in *.
  intro. apply n. subst. reflexivity.
Qed.
            
Lemma eval_at_preserves_sub:
  forall t t' s s' A ,
    sub nil t s ->
    eval_at (t, A) t' ->
    eval_at (s, A) s' ->
    ok_type nil t' A ->
    sub nil t' s'.
Proof.
  intros t t' s s' A H.
  revert t' s' A.
  induction H; intros.
          assert (Hx := eval_at_fun _ _ _ _ H H0).
          subst.
          eauto.
        inversion H.
      inversion H0; subst.
      eauto.
    destruct S.
    destruct (sub_tlc_implies_tlc _ _ _ _ H eq_refl).
    subst.
    inversion H1; subst.
    destruct (sub_tlc_implies_tlc _ _ _ _ H0 eq_refl).
    subst.
    inversion H2; subst.
    eauto.
    inversion H1; subst.
    destruct (type_dec (t_X t) T).
      subst.
      destruct (type_dec (t_X t) U).
        subst.
        eauto.
      eauto.
    destruct (type_dec T (t_C Object)).
      subst.
      assert (Hs := sub_object_object _ _ _ H0 eq_refl).
      subst.
      inversion H2; subst.
      eauto.
    exfalso. apply (sub_nil_var _ _ _ H eq_refl H4).
      assumption.
    destruct (sub_nested_t _ _ _  H (tin1 s s0)).
      subst.
      inversion H1; subst.
      eauto.
    subst.
    eauto.
    destruct (type_dec (t_XdotC t s) T).
      subst.
      inversion H1; subst.
      eauto.
    destruct (type_dec T (t_C Object)).
      subst.
      assert (Hs := sub_object_object _ _ _ H0 eq_refl).
      subst.
      inversion H2; subst.
      eauto.    
    exfalso. apply (sub_nil_var_nested _ _ _ _ H eq_refl H4).
      assumption.
    destruct (sub_nested_t _ _ _ H (tin3 s)).
      subst. 
      eauto.
    subst.
    eauto.
  inversion H0; subst.
  inversion H1; subst.
  eauto.
Qed.

(*
Lemma field_inheritance:
  forall (C0 : type) (f0 : fieldname) (T t0 A C' : type),
    inheritance nil t0 C0 ->
    ok_type nil t0 A ->
    eval_at (t0, A) C' ->
    field C0 f0 T -> field C' f0 T.
Proof.
  intros C0 f0 T t0 A C' H.  
  revert f0 T A C'.
  induction H; intros.
      inversion H1; subst.
      inversion H2; subst.
      case (C == D).
        intro.
        subst.
        assumption.
      intro.
      unfold field.
      assert (exists C' fs c ms ns, binds C (C',fs,c,ms,ns) CT).
        admit.
      destruct H5 as [C' [fs [c [ms [ns H5]]]]].
      destruct (sub_fields _ _ _ _ _ (tiq_C C) H H3 H0).
      exists (x ++ x0).
      assumption.
      apply binds_head.
      assumption.
    inversion H2; subst.
    inversion H3; subst.
    case (C == D).
      intro.
      subst.
      assumption.
    intro.
    unfold field.
    admit.
  inversion H1.
  inversion H2.
Qed.
*)

(*
Lemma ea_substitutivity_nested':
  forall C D xTs b U A A' t0 ts xts,
    typing nil ((this, t_dotC D) :: xTs) b U A' ->
    typeis_qcname A ->
    ok_type nil (t_CdotC C D) A -> (* removes type arguments *)
    env_zip xTs ts xts ->
    eval_at (U, t_CdotC C D) t0 ->
    eval_ats (imgs xTs) (t_CdotC C D) ts ->
    typing nil ((this, t_CdotC C D) :: xts) b t0 A.
Proof.
  intros C D xTs b.
  revert C D xTs.
  induction b using exp_ind2;
    intros.

        inversion H; subst.
        case (v == this).
          intro.
          subst.
          inversion H10; subst.
          rewrite eq_atom_true in H8.
          subst injections.
          inversion H3; subst.
          apply t_var; eauto.
            apply (ok_env_zip _ _ _ _ _ _ H4 H2 H7).
          apply binds_first.
        intro.
        inversion H10; subst.
        rewrite eq_atom_false in H8; eauto.
        assert (binds v U xTs).
          unfold binds.
          assumption.
        assert (Hb := binds_env_zip' _ _ _ _ _ _ _ H5 H4 H3 H2).
        apply t_var; eauto.
        apply (ok_env_zip _ _ _ _ _ _ H4 H2 H7).

      inversion H; subst.
      assert (B = C0).
        destruct B; inversion H9; subst; eauto.
          inversion H11.
        inversion H14.
      subst.
      assert (exists S, eval_at (T0, t_CdotC C D) S /\
                        eval_at (T, S) t0).
        inversion H7; subst.
          destruct T0; inversion H13; subst.
                exists (t_C s).
                destruct T; inversion H10; subst; 
                inversion H3; subst; eauto.
              inversion H8.
              inversion H5.
            exists (t_CdotC s s0).
            destruct T; inversion H10; subst; 
            inversion H3; subst; eauto.
          inversion H8.
          inversion H5.
        destruct T0; inversion H13; subst.
                exists (t_C s).
                destruct T; inversion H10; subst; 
                inversion H3; subst; eauto.
              inversion H8.
              inversion H5.
            exists (t_CdotC s s0).
            destruct T; inversion H10; subst; 
            inversion H3; subst; eauto.
          inversion H8.
          inversion H5.
        exists (t_CdotC C s).
        destruct T; inversion H10; subst; 
        inversion H3; subst; eauto.        
      destruct H5 as [S [Ha Hb]].
      assert (IH := IHb _ _ _ _ _ _ _ _ _ H16 H0 H1 H2 Ha H4).
      assert(exists C0', eval_at (S, A) C0' /\ 
                         inheritance nil C0' C0).
        destruct T0.
                inversion Ha; inversion H13; subst; eauto.
              inversion H13; subst. 
              inversion H8. inversion H5.
            inversion Ha; inversion H13; subst.
            exists (t_CdotC s s0).
            split.
              eauto.
            eapply inh_nested; eauto.
          inversion H13; subst.
          inversion H8. inversion H5.
        inversion Ha; subst.
        exists (t_CdotC C s).
        split.
          eauto.
        admit.
      destruct H5 as [C0' [H5 H6]].
      assert (eval_at (C0', A) C0'). admit.
      assert (ok_type nil C0' A). admit.
      assert (Hf := field_inheritance _ _ _ _ _ _ H6 H12 H11 H8).
      assert (eval_bound nil C0' C0').
        destruct C0'; eauto.
            inversion Hf. inversion H14.
          inversion Hf. inversion H14.
        inversion Hf. inversion H14.
      eapply t_field; eauto. 

    inversion H0; subst.
    assert (eval_at (T0, t_CdotC C D) t0).
      admit.
    assert (eval_ats (imgs xTs) (t_CdotC C D) ts).
      admit.
    assert (IH := IHb C _ _ _ _ _ t0 _ _ H25 H1 H2 H3 H6 H5).
    assert (typeis_qcname C0).
      inversion H19; subst; eauto.
    assert (Hm := method_benv_nil _ _ _ _ _ _ H18).
    subst.
    inversion H14; subst.
    rewrite H15 in *.
    apply keys_l_nil in H15.
    subst.
    rewrite subst_types_nil in *.
    unfold subst_type in *.
    assert (B = C0).
      inversion H19; subst; eauto.
        inversion H19; subst.
        inversion H20.
      inversion H19; subst.
      inversion H17.
    subst.
    clear H27; clear H11; clear H14.
    simpl in *.
    assert (eval_at (subst_type nil U0, C0) t0). admit.
    assert (eval_ats (subst_types nil (imgs xTs)) C0 ts). admit.
    assert (method m C0 nil U0 xTs b0). admit.
    assert (eval_bound nil C0 C0).
      inversion H8; subst; eauto.
    assert (eval_at (C0, A) C0). admit.
    assert (typing nil ((this, t_CdotC C D) :: xts) b C0 A). admit.
    assert (wide_typings nil ((this, t_CdotC C D) :: xts) l0 ts A). admit.
    apply (t_invk _ _ nil U0 C0 _ ts (imgs xTs) nil nil
                  _ xTs _ _ C0 C0 _ _ b0); eauto.

  inversion H0; subst.
  assert (U = t0).
    destruct U; inversion H4; subst; eauto.
    inversion H9. 
  subst.
  apply (t_new _ fs _ _ _ _ ts0); eauto.
  admit.
  Grab Existential Variables.
  apply b. apply C. apply xTs.
Qed.
*)

Lemma ea_substitutivity_nested:
  forall C D xTs b U A A' t0 ts xts,
    wide_typing nil ((this, t_dotC D) :: xTs) b U A' ->
    typeis_qcname A ->
    ok_type nil (t_CdotC C D) A ->
    env_zip xTs ts xts ->
    eval_at (U, t_CdotC C D) t0 ->
    eval_ats (imgs xTs) (t_CdotC C D) ts ->
    wide_typing nil ((this, t_CdotC C D) :: xts) b t0 A.
Proof.
  intros C D xTs b.
  revert C D xTs.
  induction b using exp_ind2;
    intros.
        admit. (* e_var *)
      admit. (* e_field *)
    admit. (* e_invk *)
  admit. (* e_new *)
Qed.

Lemma env_zip_equal:
  forall (ts ts':tenv),
    env_zip ts (imgs ts) ts' -> ts = ts'.
Proof.
  intro ts.
  induction ts; intros.
    inversion H; subst.
    reflexivity.
  destruct ts'.
    inversion H; subst.
  inversion H; subst.
  rewrite (IHts ts' H1).
  reflexivity.
Qed.

Lemma method_implies_ok:
  forall m C D E t tE e A,
    method m (t_CdotC C D) E t tE e ->
    typeis_qcname A ->
    ok_type E (t_CdotC C D) A.
Proof.
  intros m C D E t tE e A H.
  revert A.
  induction H;
    intros;
    eauto.
Qed.

(** * Preservation property *)
Theorem preservation: 
  forall E tE e e' t A,
    E = nil -> (* removes type arguments *)
    typing E tE e t A ->
    eval e e' ->
    wide_typing E tE e' t A.
  Proof.
    intros E tE e e' t A HE H H0.
    generalize dependent t.
    induction H0;
      intros.
    
        inversion H2; subst.  (* e_field case *)
        inversion H14; subst.
        apply (Facts1.fields_fun T0 fs0 fs) in H;
          eauto; subst.
        destruct H6; subst.
        assert (Hqcn : typeis_qcname T0).
          inversion H10; subst; eauto.
        inversion Hqcn; subst.
          inversion H11; subst.
          inversion H7; subst.
          apply (Facts1.fields_fun (t_C C) x fs) in H;
            eauto; subst.
          destruct (binds_zip' _ _ _ _ _ _ t _ _ _ _ H5 H15 H18 H0 H3 H8).
          assert (x = e) by (eapply binds_fun; eassumption). 
          subst. 
          assumption.
        inversion H11; subst.
        inversion H7; subst.
        apply (Facts1.fields_fun (t_CdotC C D) x fs) in H;
          eauto; subst.        
        destruct (binds_zip' _ _ _ _ _ _ t _ _ _ _ H5 H15 H18 H0 H3 H8).
        assert (x = e) by (eapply binds_fun; eassumption). 
        subst. 
        assumption.

      subst. (* e_meth case *)
      assert (H5 := method_implies_typing'' m C E0 t tenv e H).
      destruct H5 as [t' [A' [Ht' [HA H5]]]].
      inversion H3; subst.
      inversion H23; subst.
      assert (typeis_qcname T0).
        inversion H; subst; eauto.

      inversion H2; subst. (* top class case *)
        inversion H20; subst.
        inversion H17; subst.
        destruct (method_fun _ _ _ _ _ _ _ _ _ _ H H16)
            as [Hme1 [Hme2 [Hme3 Hm4]]].
        subst.
        assert (He := env_zip_equality _ _ _ _ H1 H12 eq_refl).
        subst.

        destruct (exists_env_zip _ _ _ _ H11) as [xts H13].
        apply (term_substitutivity ((this,t_C C)::xts) _ _ _ _
                                   ((e_new (t_C C) es0)::es) _ _).
            inversion Ht'; subst.
            inversion HA; subst.
            assert (He := eval_ats_top _ _ _ _ H15 eq_refl). subst.
            assert (He := eval_ats_top _ _ _ _ H11 eq_refl). subst.
            assert (He := eval_at_top _ _ _ H10). subst.
            assert (Hnil := method_benv_nil _ _ _ _ _ _ H).
            subst.
            simpl.
            simpl in *.
            apply keys_l_nil in H12. subst.
            rewrite subst_types_nil in *.
            rewrite subst_type_exp_nil in *.
            unfold subst_type in *.
            simpl in *.
            apply env_zip_equal in H13.
            subst.
            apply (ea_substitutivity_top 
                     _ _ _ _ _ _ H5 H6 H18).
          rewrite imgs_list_app.
          apply (wts_cons _ _ _ _ _ _ _ H6).
            rewrite (env_zip_imgs _ _ _ H13).
            assumption.
          eauto.
        apply z_cons.
        apply (env_zip_zip _ _ _ _ _ H0 H13).

      (* nested class case *)
        inversion H20; subst.
        inversion H17; subst.
        destruct (method_fun _ _ _ _ _ _ _ _ _ _ H H16)
            as [Hme1 [Hme2 [Hme3 Hm4]]].
        subst.
        assert (He := env_zip_equality _ _ _ _ H1 H12 eq_refl).
        subst.

        destruct (exists_env_zip' _ _ _ _ _ H11) as [xts H13].
        apply (term_substitutivity ((this,t_CdotC C D)::xts) _ _ _ _
                                   ((e_new (t_CdotC C D) es0)::es) _ _).
            inversion Ht'; subst.
            inversion HA; subst.
            assert (Hnil := method_benv_nil _ _ _ _ _ _ H).
            subst.
            simpl in *.
            apply keys_l_nil in H12.
            subst.
            rewrite subst_types_nil in *.
            rewrite subst_type_exp_nil in *.
            unfold subst_type in *.
            simpl in *.
            inversion HA; subst.
            assert (Hm := method_implies_ok _ _ _ _ _ _ _ _ H H6).
            inversion H5; subst.
            eapply ea_substitutivity_nested; eauto.
          rewrite imgs_list_app.
          apply (wts_cons _ _ _ _ _ _ _ H6).
            rewrite (env_zip_imgs _ _ _ H13).
            assumption.
          eauto.
        apply z_cons.
        apply (env_zip_zip _ _ _ _ _ H0 H13).

    eapply preservation_over_ec; (* exp_context case *)
      eassumption.
    Qed.

(** * Progress property *)
Theorem progress':
  (forall E tE e t A, 
     typing E tE e t A -> tE = nil -> 
     value e \/ exists e', eval e e') /\
  (forall E tE e t A, 
     wide_typing E tE e t A -> tE = nil -> 
     value e \/ exists e', eval e e') /\
  (forall E tE ds env A, 
     wide_typings E tE ds env A -> tE = nil -> 
     (forall v, In v ds -> value v) \/
     exists EE e0 e0', 
       exps_context EE /\
       EE e0 = ds /\
       eval e0 e0').
Proof.
  apply typings_mutind;
  intros; 
  subst; 
  specialize trivial.
              contradiction (binds_nil H1). (* binds ... nil *)

            right. (* eval field *)
            destruct H5.
              inversion H5; subst.
              destruct H0.
              inversion H4; subst.
              inversion H6; subst.
                inversion H3; subst.
                inversion H1; subst.
                apply Facts1.fields_fun with (fs:=x) in H12; 
                  eauto; subst.
                destruct (exists_env_zip_fields _ _ _ _ _ _ H18 H15)
                  as [xes He].
                destruct (exists_binds _ _ _ _ _ H8 He) as [e H10].
                eauto.
              inversion H3; subst.
              inversion H1; subst.
              apply Facts1.fields_fun with (fs:=x) in H12; 
                eauto; subst.
              destruct (exists_env_zip_fields _ _ _ _ _ _ H18 H15)
                as [xes He].
              destruct (exists_binds _ _ _ _ _ H8 He) as [e H12].
              eauto.
            destruct H5 as [e' H5].
            inversion H5; subst; eauto.

          right. (* eval meth *)
          destruct H11.
            inversion H4; subst.
            inversion H10; subst.
            inversion H5; subst.
              inversion H9; subst.
              inversion H8; subst.
              destruct (exists_env_zip_method _ _ _ _ _ _ _ H12 H2)
                as [ves Hx].
              destruct (exists_env_zip_subs _ _ _ H14) as [XTs Hy].
              exists (subst_exp ((this,e_new (t_C C0) es0)::ves)
                                (subst_type_exp XTs b)).
              eauto.
            inversion H9; subst.
            inversion H8; subst.
            destruct (exists_env_zip_method _ _ _ _ _ _ _ H12 H2)
              as [ves Hx].
            destruct (exists_env_zip_subs _ _ _ H14) as [XTs Hy].
            exists (subst_exp ((this,e_new (t_CdotC C0 D) es0)::ves)
                              (subst_type_exp XTs b)).
            eauto.
          destruct H4 as [e' H4].
          assert (HEE := esc_head es).
          remember (fun e : exp => e :: es) as EE.
          assert (Hem := ec_meth_arg0 m es (imgs XPs)).
          remember (fun e0 : exp => e_meth e0 m (imgs XPs) es) as EE'.
          assert (Hec := eval_context EE' e0 e' H4 Hem).
          inversion H4; subst;
            eauto.
              
        (* value new ...*)
        assert (typeis_qcname A0).
          inversion H0; subst; eauto.
        destruct H3 as [H3 | [EE [e0 [e0' [H5 [H6 H7]]]]]].
          eauto.
        subst.
        right.
        eauto.

      assumption.
    left. intros. inversion H2; subst.
  destruct H3; subst.
    destruct H1; subst.
      left.
      intros.
      destruct (exp_dec e v).
        subst.
        assumption.
      apply H1.
      unfold In in H4.
      destruct H4.
        unfold not in H5.
        exfalso.
        apply H5. 
        assumption.
      assumption.
    right.
    destruct H1 as [EE [e0 [e0' [Hx [Hy Hz]]]]].
    subst.
    assert (HEE := esc_tail e EE Hx).
    exists (fun e0 : exp => e :: EE e0), e0, e0'.
    split; eauto.
  destruct H3 as [e' H3].
  destruct H1; subst.
    right.
    assert (HEE := esc_head es).
    exists (fun e : exp => e :: es), e, e'.
    eauto.
  right.
  assert (HEE := esc_head es).
  exists (fun e : exp => e :: es), e, e'.
  eauto.
Qed.

  Theorem progress: 
    forall e t A,
      typing nil nil e t A ->
      value e \/ (exists e', eval e e').
  Proof.
    intros.
    destruct progress' as [Hpro _].
    apply (Hpro nil nil e t A H eq_refl).
  Qed.

End Properties.

(** * Epilogue *)

(** Check that these properties indeed prove safety *)

Module SafetyProof : Safety := Properties.
